msg-spec-loc-decl(snd; i; da)
== k:Knd, l:IdLnk.
== (fpf-dom(product-deq(Knd; IdLnk; Kind-deq; idlnk-deq); <k, l>; snd))
==  ((source(l) = i)
==   l_all(map((p.p.1); fpf-ap(snd; product-deq(Knd; IdLnk; Kind-deq; idlnk-deq); <k, l>));
==   l_all(Id;
==   l_all(tg.(fpf-dom(Kind-deq; rcv(l,tg); da)))) 

latex

---

clarification:

msg-spec-loc-decl(snd; i; da)
== k:Knd, l:IdLnk.
== (fpf-dom(product-deq(Knd; IdLnk; Kind-deq; idlnk-deq); <k, l>; snd))
==  ((source(l) = i  Id)
==   l_all(map((p.p.1); fpf-ap(snd; product-deq(Knd; IdLnk; Kind-deq; idlnk-deq); <k, l>));
==   l_all(Id;
==   l_all(tg.(fpf-dom(Kind-deq; rcv(l,tg); da)))) 

latex

Definitions	x:A. B(x), P  Q, P  Q, s = t, source(l), l_all(L; T; x.P(x)), map(f; as), x.A(x), t.1, fpf-ap(f; eq; x), product-deq(A; B; a; b), Knd, IdLnk, idlnk-deq, <a, b>, Id, b, fpf-dom(eq; x; f), Kind-deq, rcv(l,tg)
FDL editor aliases	msg-spec-loc-decl